A:Type, eq:EqDecider(A), B:(AType), L:(a:A fp B(a) List), x:A.
(x  dom((L)))  (fL.(x  dom(f)) & (L)(x) = f(x)  B(x)) 

latex

Definitions	x:A. B(x), b, t  T, f(a), x(s), a:A fp B(a), s = t, x:A  B(x), P & Q, (xL.P(x)), P  Q, (L), False, type List, x:AB(x), Type, EqDecider(T), left + right, P  Q, Dec(P), x. t(x), P  Q, (x  l), if b then t else f fi , , A c B, x.A(x), f(x), f  g, P  Q, x  dom(f), {x:A| B(x)} , <a, b>, A, b, , Unit, {T}, Top, x:A. B(x), a < b
Lemmas	fpf-join wf, fpf-trivial-subtype-top, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, fpf-join-ap, fpf-dom wf, l exists wf, l member wf, l exists cons, fpf-ap wf, fpf-join-dom, decidable assert, assert wf